User blog:Vel!/BB(n) in FOST
Work in progress, but you know how I never finish what I sta I'm slowly assembling all the pieces for writing \(\Sigma(n)\) in first-order set theory. Since \(\Sigma(n)\) is a well-known and well-respected function, it'd be nice to bound Rayo's function with it despite having Xi and FGH. This code is an abstraction of what the final FOST formula will look like; I'll be writing a short paper on this bound. N is a fixed positive integer written into the final formula. // Halting state HALT = N // States, not including halt States* = N // States, including halt States = N ∪ {HALT} = N + 1 // Colors Colors = {0, 1} // Left and Right movements. The values don't matter as long as they're different. Moves = {L, R} L ≠ R IsRuleset?(func) -> Is func a ruleset for a 2-color N-state TM? // Ensure that all members of the function are of the form ((State, Color), (State', Color', Move)) // Note that (a, b, c) is a shortcut for (a, (b, c)) ∀x: x ∈ func ⇔ (∃s,c,s',c',m: x = ((s, c), (s', c', m)) ∧ s ∈ States* ∧ c ∈ Colors ∧ s' ∈ States ∧ c' ∈ Colors ∧ m ∈ Moves) // Ensure that for each (State, Color) there is exactly one (State', Color', Move) ∀s: ∀c: (s ∈ States* ∧ c ∈ Colors) → (∃s',c',m: s' ∈ States* ∧ c' ∈ Colors ∧ m ∈ Moves (∀x: ((s, c), x) ∈ func ⇔ x = (s', c', m))) IsTape?(func) -> Is func a 2-color tape? // Ensure that all members of the function are of the form (Pos, Color) ∀x: x ∈ func ⇔ (∃p,c: x = (p, c) ∧ p ∈ ω ∧ c ∈ Colors) // Ensure that for each Pos there is exactly one Color ∀p: p ∈ ω → (∃c: c ∈ Colors ∧ (∀x: (p, x) ∈ func ⇔ x = c)) InitializeTape() -> (tape) Creates a zero-filled tape. ∀x: x ∈ tape ⇔ (∃p: (p, 0) = x ∧ p ∈ ω) Shift(tape, fill) -> (tape') Shifts the tape over by one step, adding a zero at the left. ∀x: x ∈ tape' ⇔ ((∃p,c: (Sp, c) = x ∧ (p, c) ∈ tape) ∨ (x = (0, fill))) Read(tape, position) -> (color) Read a color at a certain position. (position, color) ∈ tape Write(tape, position, color) -> (tape') Write a color at a certain position. ∀x: x ∈ tape' ⇔ (∃p,c: (p, c) = x ∧ ((p ≠ position ∧ (p, c) ∈ tape) ∨ (p = position ∧ c = color))) // This is an example of an if statement in FOST Transition(ruleset, tape, state, position) -> (tape', state', position') Simulates one step of a Turing machine with a given ruleset, returning the altered tape, state, and position. (state', color', move) = Apply(ruleset, (state, Read(tape, position))) ∧ (tape' = Shift(Write(tape, position, color'), 0)) ∧ ((move = L ∧ position' = position) ∨ (move = R ∧ position' = S(S(position)))) Steps(ruleset) -> (steps) Simulates a Turing machine, returning a set with all the steps. ∀tape',state',pos': (tape', state', pos') ∈ Steps ⇔ (IsTape?(tape') ∧ state' ∈ States ∧ pos' ∈ ω ∧ ((tape' = InitializeTape() ∧ state' = 0 ∧ pos' = 0) ∨ (∃tape,state,pos: (tape, state, pos) ∈ Steps ∧ IsTape?(tape) ∧ state ∈ States* ∧ pos ∈ ω ∧ Transition(ruleset, tape, state, pos) = (tape', state', pos')))) Output(ruleset) -> (output) ∀tape',count': (tape', count') ∈ CountOnes ⇔ (IsTape?(tape') ∧ count' ∈ ω ∧ ((tape' = InitializeTape() ∧ count' = 0) ∨ (∃tape,count: (tape, count) ∈ Steps ∧ IsTape?(tape) ∧ count ∈ ω ∧ ((tape' = Shift(tape, 0) ∧ count' = count) ∨ (tape' = Shift(tape, 1) ∧ count' = S(count)))))) (∃t,p: (t, HALT, p) ∈ Steps(ruleset) ∧ (output = Apply(CountOnes, t))) ∨ (¬∃t,p: (t, HALT, p) ∈ Steps(ruleset) ∧ (output = 0)) ∀ruleset: IsRuleset?(ruleset) ⇔ Output(ruleset) ∈ Outputs T = Max(Outputs) FOST feels like a stone-age ancestor of Scheme. Someday we'll have a program that compiles a dialect of Scheme into FOST. Category:Blog posts